T:Type, eq:EqDecider(T), as, bs:T List, x:T. (x  l-union(eq;as;bs))  (x  as)  (x  bs) 

latex

Definitions	l-union(eq;as;bs), Type, t  T, x:A. B(x), EqDecider(T), type List, False, x:AB(x), P  Q, x:AB(x), P & Q, P  Q, left+right, P  Q, nil, (x  l), P  Q, Prop, s = t, car.cdr, insert(a;L), {T}
Lemmas	member-insert, insert wf, iff functionality wrt iff, or functionality wrt iff, cons member, l-union wf, l member wf, nil member, deq wf